p:FinProbSpace, a:, n:. E(n;a) = a 

latex

Definitions	rv-const(a), t  T, x:A. B(x), Outcome, {x:A| B(x)} , , x:AB(x), #$n, {i..j}, Type, f(a), <a, b>, , s = t, P  Q, False, A, A  B, , FinProbSpace, E(n;F)
Lemmas	nat wf, rationals wf, finite-prob-space wf, expectation-constant, rv-const wf, int seg wf, p-outcome wf